We consider the problem of existential quantifier elimination for Booleanformulas in Conjunctive Normal Form (CNF). We present a new method for solvingthis problem called Derivation of Dependency-Sequents (DDS). ADependency-sequent (D-sequent) is used to record that a set of quantifiedvariables is redundant under a partial assignment. We introduce aresolution-like operation called join that produces a new D-sequent from twoexisting D-sequents. We also show that DDS is compositional, i.e. if our inputformula is a conjunction of independent formulas, DDS automatically recognizesand exploits this information. We introduce an algorithm based on DDS andpresent experimental results demonstrating its potential.
展开▼
